Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    ap(ap(map,f),xs)  → ap(ap(ap(if,ap(isEmpty,xs)),f),xs)
2:    ap(ap(ap(if,true),f),xs)  → null
3:    ap(ap(ap(if,null),f),xs)  → ap(ap(cons,ap(f,ap(last,xs))),ap(ap(if2,f),xs))
4:    ap(ap(if2,f),xs)  → ap(ap(map,f),ap(dropLast,xs))
5:    ap(isEmpty,null)  → true
6:    ap(isEmpty,ap(ap(cons,x),xs))  → null
7:    ap(last,ap(ap(cons,x),null))  → x
8:    ap(last,ap(ap(cons,x),ap(ap(cons,y),ys)))  → ap(last,ap(ap(cons,y),ys))
9:    ap(dropLast,ap(ap(cons,x),null))  → null
10:    ap(dropLast,ap(ap(cons,x),ap(ap(cons,y),ys)))  → ap(ap(cons,x),ap(dropLast,ap(ap(cons,y),ys)))
There are 16 dependency pairs:
11:    AP(ap(map,f),xs)  → AP(ap(ap(if,ap(isEmpty,xs)),f),xs)
12:    AP(ap(map,f),xs)  → AP(ap(if,ap(isEmpty,xs)),f)
13:    AP(ap(map,f),xs)  → AP(if,ap(isEmpty,xs))
14:    AP(ap(map,f),xs)  → AP(isEmpty,xs)
15:    AP(ap(ap(if,null),f),xs)  → AP(ap(cons,ap(f,ap(last,xs))),ap(ap(if2,f),xs))
16:    AP(ap(ap(if,null),f),xs)  → AP(cons,ap(f,ap(last,xs)))
17:    AP(ap(ap(if,null),f),xs)  → AP(f,ap(last,xs))
18:    AP(ap(ap(if,null),f),xs)  → AP(last,xs)
19:    AP(ap(ap(if,null),f),xs)  → AP(ap(if2,f),xs)
20:    AP(ap(ap(if,null),f),xs)  → AP(if2,f)
21:    AP(ap(if2,f),xs)  → AP(ap(map,f),ap(dropLast,xs))
22:    AP(ap(if2,f),xs)  → AP(map,f)
23:    AP(ap(if2,f),xs)  → AP(dropLast,xs)
24:    AP(last,ap(ap(cons,x),ap(ap(cons,y),ys)))  → AP(last,ap(ap(cons,y),ys))
25:    AP(dropLast,ap(ap(cons,x),ap(ap(cons,y),ys)))  → AP(ap(cons,x),ap(dropLast,ap(ap(cons,y),ys)))
26:    AP(dropLast,ap(ap(cons,x),ap(ap(cons,y),ys)))  → AP(dropLast,ap(ap(cons,y),ys))
The approximated dependency graph contains 3 SCCs: {24}, {26} and {11,12,15,17,19,21}.
Tyrolean Termination Tool  (0.31 seconds)   ---  May 3, 2006